%\shortv{\noindent {\bf Termination is Decidable in \ahopi.}}
%\longv{
\subsection{Termination is Decidable in \hof}
%}
Here we prove that termination is decidable in \hof. 
%We shall exploit the proof strategy in \cite{BusiGZ09} which is based on results obtained for WSTS. %
The crux of the proof consists in finding an upper bound for a process and its derivatives. This is possible in $\hof$ because of the limited structure allowed in output actions. 
\longv{

}
%More in details, w
We proceed as follows. 
First we define a notion of \emph{normal form} for \hof processes. We then characterize an upper bound for the derivatives of a given process, and define an ordering over them. 
This ordering is then shown to be a wqo that is strongly compatible with respect to the LTS of \hof given in Section \ref{ss:lts}. 
The decidability result is then obtained by resorting to the 
%results from \cite{FinkelS01} reported before.
theory of well-structured transition systems introduced in Section \ref{ss:wsts}.


\begin{definition}[Normal Form] \label{def:nf}
Let $P \in \hof$. $P$ is in \emph{normal form} iff 
%{\small 
%\vspace{-2mm} 
$$P = \prod_{k=1}^{l} x_k \parallel \prod_{i=1}^{m} a_i(y_i) . P_i \parallel \prod_{j=1}^{n} \Ho{b_j}{P'_j}$$ % \vspace{-2mm} $$
%}
where each $P_i$ and $P'_j$ are in normal form. 
\end{definition}


\begin{lemma}\label{lem:nf}
 Every process $P \in \hof$ is structurally congruent to a normal form.
\end{lemma}
%\shortv{
%\begin{proof}\vspace{-1.5mm}
%By induction on the structure of $P$. 
%\qed \end{proof}
%}
\longv{
\begin{proof}
By induction on the structure of $P$. The base cases are when $P = \nil$ and when $P = x$, and are immediate.
Cases $P = \Ho{a}{Q}$ and $P = a(x).Q$ follow by applying the inductive hypothesis on $Q$. 
For the case $P = P_1 \parallel P_2$, we apply the inductive hypothesis twice and we obtain that 
%\begin{eqnarray*}
\[
P_1  \equiv  \prod_{k = 1}^{l} x_k \parallel \prod^{m}_{i = 1} a_i(y_i).P_i \parallel \prod^{n}_{j = 1}\Ho{b_j}{P_j} ~~ \mbox{and} ~~
P_2  \equiv  \prod_{k = 1}^{l'} x_k \parallel \prod^{m'}_{i = 1} a'_i(y'_i).P'_i \parallel \prod^{n'}_{j = 1}\Ho{b'_j}{P'_j} \, . \]
%\end{eqnarray*}
It is then easy to see that  $P_1 \parallel P_2$ 
%\[
%P_1 \parallel P_2 =   \prod_{k = 1}^{l} x_k \parallel \prod_{k = 1}^{l'} x_k \parallel \prod^{m}_{i = 1} a_i(y_i).P_i \parallel \prod^{m'}_{i = 1} a'_i(y'_i).P'_i \parallel \prod^{n}_{j = 1}\Ho{b_j}{P_j} \parallel \prod^{n'}_{j = 1}\Ho{b'_j}{P'_j}
%\]
is structurally congruent to a normal form, as desired.
\qed \end{proof}
}

We now define an ordering over normal forms. Intuitively, a process is larger than another if it has more parallel components.

\begin{definition}[Relation $\preceq$]\label{d:order}
Let $P,Q \in \hof$. We write $P \preceq Q$ iff there exist $x_1\dots x_l$, $P_1 \dots P_m$, $P'_1 \dots P'_n$, $Q_1 \dots Q_m$, $Q'_1 \dots Q'_n$, and $R$ such that 
\[
\begin{array}{lll}
P & \equiv &  \prod_{k=1}^{l} x_k \parallel \prod_{i=1}^{m} a_i(y_i) . P_i \parallel \prod_{j=1}^{n} \Ho{b_j}{P'_j}\\
Q & \equiv & \prod_{k=1}^{l} x_k \parallel \prod_{i=1}^{m} a_i(y_i) . Q_i \parallel \prod_{j=1}^{n} \Ho{b_j}{Q'_j} \parallel R
\end{array}
\]

with $P_i \preceq Q_i$ and $P'_j \preceq Q'_j$, for $i \in [1..m]$ and $j \in [1..n]$.
\end{definition}

The normal form of a process can be intuitively represented in a tree-like manner.
More precisely, given the process in normal form 
%{\small \vspace{-2mm}
\[P = \prod_{k=1}^{l} x_k \parallel \prod_{i=1}^{m} a_i(y_i) . P_i \parallel \prod_{j=1}^{n} \Ho{b_j}{P'_j}\] %\vspace{-2mm} \]
%}
we shall decree its associated tree to have a root node labeled $x_1,\ldots,x_k$.
This root node has $m+n$ children, corresponding to the  trees associated to processes $P_1, \ldots, P_m$ and 
$P'_1, \ldots, P'_m$; the outgoing edges connecting the root node and the children 
are labeled $a_1(y_1),$ $\ldots, a_m(y_m)$ and $\overline{b_1}, \ldots, \overline{b_n}$.

\longv{
\begin{example}\label{ex:tree}
Process $P = x \parallel a(y).(b.y \parallel c) \parallel \Ho{a}{z \parallel d.e}$ has the following
tree representation:
 \input{treeproc}
\end{example}
}

%The intuition given before 
This intuitive representation of 
%on the tree representation of a 
processes in normal form as trees will be  useful to
reason about the structure of \hof terms. We begin by defining the \emph{depth} of a process. 
Notice that such a depth corresponds to the maximum depth of its tree representation.

%considered tree representation of processes
%described above. 
%rather natural notion of depth for processes in normal form.

\begin{definition}[Depth]\label{d:depth}
Let $P = \prod_{k=1}^{l} x_k \parallel \prod_{i=1}^{m} a_i(y_i) . P_i \parallel \prod_{j=1}^{n} \Ho{b_j}{P'_j}$ be a \hof process in normal form. The \emph{depth} of $P$ is given by 
%{\small 
$$\depth{P} = \max \{1+ \depth{P_i}, 1+ \depth{P'_j} \mid i \in [1..m] \wedge j \in [1..n]\}.$$
%}
\end{definition}

%The following definition formalizes the notion of the set of processes, bounded to 
Given a natural number $n$ and  
%More precisely, given 
a process $P$, the set $\mathcal{P}_{P,n}$ 
contains all those processes in normal form that %(i) 
can be built using the  alphabet of $P$ and %(ii) 
whose depth is at most $n$.


\begin{definition}\label{def:part}
 Let $n$ be a natural number and $P \in \hof$. We define the set $\mathcal{P}_{P,n}$ as follows:
%{\small
$$ \begin{array}{lll} 
%\mathcal{P}_{P,0} =& \{ \prod_{k\in K} x_k \mid & x_k \in A(P) \} \\ 
\mathcal{P}_{P,n} =& \{ Q \mid & Q \equiv  \prod_{k\in K} x_k \parallel \prod_{i \in I} a_i(y_i) . Q_i \parallel \prod_{j \in J} \Ho{b_j}{Q'_j} \\
&\ &  \wedge \  \mathcal{A}(Q) \subseteq \mathcal{A}(P) \\
& \ & \wedge \ Q_i, Q'_j \in \mathcal{P}_{P,n-1} \ \forall i \in I, j\in J \}  
\end{array}
$$
%}
where $\mathcal{P}_{P,0}$ contains processes that are built out only of variables in $\mathcal{A}(P )$.
\end{definition}

As it will be shown later, the set of all derivatives of $P$ is a subset of $\mathcal{P}_{P,2 \cdot \depth{P}}$.

When compared to processes in languages such as CCS, higher-order processes have a more complex structure. This is because, 
by virtue of reductions, an arbitrary process can take the place of possibly several occurrences of a single variable.
As a consequence, the depth of (the syntax tree of) a process cannot be determined (or even approximated) before its execution: it can vary arbitrarily along reductions. 
Crucially, in \hof it is possible to bound such a depth. Our approach is the following:
rather than solely depending on the depth of a process, we define measures on the relative position of variables within a process. Informally speaking, such a position will be determined by the number of prefixes guarding a variable.
%Notice that s
Since variables are allowed only at the top level of the output objects, their relative distance will remain 
% distance of such variables remains 
invariant during reductions.
This allows to obtain a bound on the structure of \hof processes.
Finally, it is worth stressing that even if the same notions of normal form, depth, and distance can be defined for \hocore, a finite upper bound for such a language does not exist. 
\longv{

}
We first define the maximum distance between a variable and its binder.


\begin{definition}\label{d:maxdist}
Let $P = \prod_{k \in K} x_k \parallel \prod_{i \in I} a_i(y_i) . P_i \parallel \prod_{j \in J} \Ho{b_j}{P'_j}$ be a $\hof$ process in normal form. We define the \emph{maximum distance of $P$} as: %\vspace{-2mm}
%{\small
\begin{multline*}
\maxDistance{P} = \max\{\maxDist{y_i}{P_i}, \\ \maxDistance{P_i}, \maxDistance{P'_j} | i \in I, j \in J \} %\vspace{-4mm}
\end{multline*}
%}
where
%\vspace{-3mm}
%{\small 
$$
 \maxDist{x}{P}\! = \!
\begin{cases}
 1 			& \text{if $P = x$,}\\
 1+\maxDist{x}{P_z}	& \text{if $P = a(z).P_z  \wedge \ x \neq z,$} \\
 1+\maxDist{x}{P'}	& \text{if $P = \Ho{a}{P'}$,}\\
 \max \{ \maxDist{x}{R}, \maxDist{x}{Q}\} & \text{if $P = R \parallel Q$,}\\
 0			& \text{otherwise.}
\end{cases}
$$
%}
\end{definition}

\begin{lemma}[Properties of maxDistance]\label{lem:maxdist}
 Let $P$ be a closed $\hof$ process. It holds that:%\vspace{-1mm}
\begin{enumerate}
\item $\maxDistance{P} \leq \depth{P}$ 
\item For every $Q$ such that $P \newarr Q$,  $\maxDistance{Q}  \leq \maxDistance{P}$. %\vspace{-2mm}
\end{enumerate}
\end{lemma}
% \shortv{
% \begin{proof}[Sketch]
% Part (1) is immediate from Definitions \ref{d:depth} and \ref{d:maxdist}. Part (2) follows by a case analysis on $\arro{\alpha}$.
% \qed 
% \end{proof}
% }

\longv{
\begin{proof}
Part (1) is immediate from Definitions \ref{d:depth} and \ref{d:maxdist}. Part (2) follows by a case analysis on the rule used to infer $\newarr$.
We focus in the case \textsc{Tau1}: the other cases are similar or simpler. 
We then have that 
$P = P_1 \parallel P_2$ %, $P' = P'_1 \parallel P'_2 \sub{R}{x}$, 
with $P_1 \newarro{\Ho{a}{S}} T$ and $P_2 \newarro{a(x)} R$.
Hence $P_1 \equiv \outC{a}\langle S \rangle \parallel T$ and
$P_2 \equiv a(x).R$.
We then have that 
$P \equiv \Ho{a}{S} \parallel T \parallel a(x).R$ and 
$Q \equiv R \sub S x \parallel T$.
Applying Definition \ref{d:maxdist} in both processes, we obtain
\begin{eqnarray*}
\maxDistance{P} & = & \max\{ \maxDistance{S}, \maxDist{x}{R}, \\ 
& & \qquad \quad \maxDistance{R}, \maxDistance{T}\} \\
\maxDistance{Q} & = & \max\{ \maxDistance{R \sub S x}, \maxDistance{T}\} \, .
\end{eqnarray*}
We can disregard the contribution of $\maxDistance{T}$, since it does not participate in the synchronization.
We then focus on determining $\maxDistance{R \sub S x}$. 
Notice that the only way in which the value of 
$\maxDistance{R \sub S x}$ 
could be greater than that of
$\maxDistance{R}$ is if $S$ involves some free variables that get
captured by an (input) binder in $R$ by virtue of the substitution.
Since $S$ is a closed process, it has no free variables,
and this capture is not possible.
Consequently, we have 
% We begin by recalling that by the syntax of \hof, 
% $S \equiv x_1 \parallel \cdots \parallel x_k \parallel S'$, where $S'$ is a closed process.
% The free variables in $S$ can affect $\maxDistance{R \sub S x }$ in essentially two ways:
% 
% \begin{enumerate}
% \item \emph{The free variables of $S$ do not get captured by a binder in $R$}. In this case, they do not contribute to 
% $\maxDistance{R \sub S x}$, and we have that 
\[
 \maxDistance{R \sub S x} \leq \max \{ \maxDistance{R}, \maxDistance{S} \}
\]
and the thesis holds.
% 
% \item \emph{Some of the free variables of $S$ get captured by a binder in $R$}.
% In this case we find it convenient to appeal to the tree representations of $R$ and $S$, denoted
% $T_R$ and $T_S$, respectively. Notice that $T_S$ is a tree where the root node is labeled with $x_1, \ldots, x_k$ and 
% whose only descendant is
% $T_S'$, the tree representation of $S'$.
% Consider now $T_{Q}$, 
% the  tree representation of $R \sub S x$: it corresponds to the tree $T_R$ 
% in which all occurrences of $x$ in the nodes of $T_R$ have been replaced with $T_S$. 
% Crucially, the height of $x_1, \ldots, x_k$ is exactly the same height 
% of $x$, so the distance with respect their binder does not increase. 
% Also, since $S'$ does not contain free variables, 
% the contribution of $\maxDistance{S'}$ to $P$ remains invariant in $Q$.  
% We then conclude that the thesis holds also in this case.
% \end{enumerate}
\qed 
\end{proof}
}





We now define the maximum depth of processes that can be communicated.
Notice that the continuations of inputs are considered as 
along reductions
they could become communication objects themselves:

\begin{definition}\label{d:maxdepcom}
Let $P = \prod_{k \in K} x_k \parallel \prod_{i \in I} a_i(y_i) . P_i \parallel \prod_{j \in J} \Ho{b_j}{P'_j}$ be a $\hof$ process in normal form. We define the \emph{maximum depth} of a process that can be communicated ($\maxDepCom{P}$) in $P$ as: %\vspace{-1mm}
% {\small
$$\maxDepCom{P} = \max\{ \maxDepCom{P_i}, \depth{P'_j} \mid i \in I, j \in J \}\ .$$
%}
\end{definition}

\begin{lemma}[Properties of maxDepCom]\label{lem:maxdepcom}
 Let $P$ be a closed $\hof$ process. It holds that:
\begin{enumerate}
 \item $\maxDepCom{P} \leq \depth{P}$
 \item For every $Q$ such that $P \newarr Q$, $\maxDepCom{Q} \leq \maxDepCom{P}$. %\vspace{-2mm}
\end{enumerate}
\end{lemma}
% \shortv{
% \begin{proof}[Sketch]
% Part (1) is immediate from Definitions \ref{d:depth} and \ref{d:maxdepcom}. 
% Part (2) follows by a case analysis on $\arro{\alpha}$.
% \qed 
% \end{proof}
%}
\longv{
\begin{proof}
Part (1) is immediate from  Definitions \ref{d:depth} and \ref{d:maxdepcom}. 
Part (2) follows by a case analysis on the rule used to infer $\newarr$.
Again, we focus in the case \textsc{Tau1}: the other cases are similar or simpler. 
We then have that 
$P = P_1 \parallel P_2$ %, $P' = P'_1 \parallel P'_2 \sub{R}{x}$, 
with $P_1 \newarro{\Ho{a}{S}} T$ and $P_2 \newarro{a(x)} R$.
Hence $P_1 \equiv \outC{a}\langle S \rangle \parallel T$ and
$P_2 \equiv a(x).R$.
We then have that 
$P \equiv \Ho{a}{S} \parallel T \parallel a(x).R$ and 
$Q \equiv R \sub S x \parallel T$.
Applying Definition \ref{d:maxdepcom} in both processes, we obtain
\begin{eqnarray*}
\maxDepCom{P} & = & \max\{ \maxDepCom{T}, \maxDepCom{S}, \\
 &  & \qquad \quad \maxDepCom{R}, \depth{S}\} \\
\maxDepCom{Q} & = & \max\{ \maxDepCom{T}, \maxDepCom{R \sub S x}\} \, .
\end{eqnarray*}
We now focus on analyzing the influence a substitution has on communicated objects.
Since variables can occur in output objects, 
the sensible case to check is if $x$
appears inside 
%More precisely, we analyze whether $x$ occurs free in 
some communication object in $R$. 
It is worth noticing that $x$ is a variable that becomes free only as a result of
the input on $a$, which consumes its binder.
We thus have two cases:

\begin{enumerate}
\item \emph{There are no communication objects in $R$ with occurrences of $x$.} 
Then, $S$ will only occur at the top level in $R \sub S x$. 
Since $\depth{S}$ was already taken into account when determining $\maxDepCom{P}$, 
we then have  that $\maxDepCom{R \sub S x} \leq \maxDepCom{P}$, and the thesis holds.

\item \emph{Some communication objects in $R$ have occurrences of $x$.} 
Then, $R$ contains as sub-process an 
output message $\Ho{b}{P_x}$ where, for some $k > 0$ and a closed process $S'$,
process $P_x \equiv \prod^k x \parallel S'$. 
%Recall that by definition of \hof, $S'$ is a closed process. 
%Therefore, t
Process $\Ho{b}{P_x \sub S x}$ then occurs in $R \sub S x$. 
Clearly, an eventual increase of $\maxDepCom{Q}$ depends on the depth of $P_x \sub S x$.
We have that $\depth{P_x \sub S x} = \max(\depth{S}, \depth{S'})$. Since both $\depth{S}$ and $\depth{S'}$
were considered when determining $\maxDepCom{P}$, we conclude that 
$\maxDepCom{R \sub S x}$ can be at most equal to $\maxDepCom{P}$, and so the thesis holds.
\end{enumerate}
\qed 
\end{proof}
}

%CHECK: reductions ($\pired$) or transitions ($\arro{\alpha}$).

%$\begin{newnotation}
%We use $P \arro{~\til \alpha~} P'$ if, for some $n \geq 0$,  there exist $\alpha_1, \ldots, \alpha_n$ such that $P \arro{\alpha_1}  \cdots \arro{\alpha_n} P'$.
%\end{newnotation}


Generalizing Lemmas \ref{lem:maxdist} and \ref{lem:maxdepcom} we obtain:

\begin{corollary}\label{c:bounddepth}
 Let $P$ be a closed $\hof$ process. For every $Q$ such that $P \newarr^* Q$, it holds that:\shortv{\vspace{-1mm}}
\begin{enumerate}
 \item $\maxDistance{Q} \leq \depth{P}$
 \item $\maxDepCom{Q} \leq \depth{P}$.
\end{enumerate}
\end{corollary}


We are interested in characterizing the derivatives of a given process $P$.
We shall show that they are over-approximated by means of the set $\mathcal{P}_{P,2 \cdot \depth{P}}$.
We will investigate the properties of the relation $\preceq$ on such an approximation; 
such properties will also hold for the set of derivatives. 


\begin{definition}
 Let $P \in \hof$. Then we define
$ \deriv{P} = \{ Q \mid P \newarr^* Q \}$
\end{definition}

The following results hold because of the limitations  we have imposed on the output actions for \hof processes.
\shortv{Any process that can be communicated in $P$ is in $\mathcal{P}_{P,n-1}$ and its maximum depth is also bounded by $\depth{P}$. The deepest position for a variable is when it is a leaf in the tree associated to the normal form of $P$. That is, when its depth is exactly $\depth{P}$.  Hence the following:} 

\longv{
\begin{lemma}\label{l:depth}
 Let $P,Q$ be \hof processes such that $\mathcal{A}(Q) \subseteq \mathcal{A}(P)$.
$Q \in \mathcal{P}_{P,n}$ if and only if $\depth{Q} \leq n$.
\end{lemma}
\begin{proof}
 The ``if'' direction is straightforward by definition of $\mathcal{P}_{P,n}$ (Definition \ref{def:part}). 

For the ``only if'' direction we proceed by induction on $n$.  If $n =0$ then $Q = \nil$ or $Q = x_1 \parallel \cdots \parallel x_k$. In both cases, 
since $\mathcal{A}(Q) \subseteq \mathcal{A}(P)$, 
$Q$ is easily seen to be in $\mathcal{P}_{P,0}$. If $n >0$ then 
\[
 Q = \prod_{k \in K} x_k \parallel \prod_{i \in I} a_i(y_i) . Q_i \parallel \prod_{j \in J} \Ho{b_j}{Q'_j}
\]
where, for every $i \in I$ and $j \in J$, both $\depth{Q_i} \leq \depth{Q} \leq n -1$ and  $\depth{Q'_j} \leq \depth{P} \leq n -1$. By inductive hypothesis, each $Q_i$ and $Q'_j$ is in $\mathcal{P}_{P,n-1}$.
Then, by Definition \ref{def:part}, $Q \in \mathcal{P}_{P,n}$ and we are done.
\qed
\end{proof}

}


\begin{proposition}\label{p:cresce}
 Let $P $ be a $\hof$ process.
Suppose, for some $R$ and $n$, that $P \in \mathcal{P}_{R,n}$. For every $Q$ such that $P \newarr Q$, it holds that 
  $Q \in \mathcal{P}_{R,2 \cdot n}$.%\vspace{-1.5mm}
\end{proposition}
% \shortv{
% \begin{proof}[Sketch]
% Recall that by Lemmata
% \ref{lem:maxdist}(1) and 
% \ref{lem:maxdepcom}(1) 
%  the maximum distance between an occurrence of a variable and its binder is bounded by $\depth{P}$. 
% By Definition \ref{def:part} any process that can be communicated in $P$ is in $\mathcal{P}_{P,n-1}$ and its maximum depth is also bounded by $\depth{P}$ (which, in turn, is bounded by $n$). 
% The deepest position for a variable is when it is a leaf in the tree associated to the normal form of $P$. That is, when its depth is exactly $\depth{P}$. 
% %Necessarily, the parent of this leaf is a process in $\mathcal{P}_{P,n-1}$.
% If in that position we place a process in $\mathcal{P}_{P,n-1}$ --- whose depth is also $\depth{P}$ --- then it is easy to see that $Q$ is in $\mathcal{P}_{P,2 \cdot n}$, and that its associated tree has a depth of $2 \cdot \depth{P}$ (which is bounded by $2 \cdot n$).
% \qed \end{proof}
% }
\longv{
\begin{proof}
We proceed by case analysis on the rule used to infer $\newarr$. 
We focus on the case such a rule is \textsc{Tau1}; the remaining cases are similar or simpler.
Recall that by Lemmas \ref{lem:maxdist}(1) and \ref{lem:maxdepcom}(1) 
 the maximum distance between an occurrence of a variable and its binder is bounded by $\depth{P}$. 
By Definition \ref{def:part} any process that can be communicated in $P$ is in $\mathcal{P}_{R,n-1}$ and its maximum depth is also bounded by $\depth{P}$  ---which, in turn, by Lemma \ref{l:depth}, is bounded by $n$. 
The deepest position for a variable is when it is a leaf in the tree associated to the normal form of $P$. That is, when its depth is exactly $\depth{P}$. 
%Necessarily, the parent of this leaf is a process in $\mathcal{P}_{P,n-1}$.
If in that position we place a process in $\mathcal{P}_{R,n-1}$ --- whose depth is also $\depth{P}$ --- then it is easy to see that (the associated tree of) $Q$ has a depth of $2 \cdot \depth{P}$, which is bounded by $2 \cdot n$.
Hence, by Lemma \ref{l:depth}, $Q$ is in $\mathcal{P}_{R,2 \cdot n}$.
\qed \end{proof}
}
The lemma below generalizes Proposition \ref{p:cresce} to a sequence of reductions.


\begin{lemma}\label{l:bound}
  Let $P $ be a $\hof$ process.
Suppose, for some $R$ and $n$, that $P \in \mathcal{P}_{R,n}$. For every $Q$ such that $P \newarr^* Q$, it holds that 
  $Q \in \mathcal{P}_{R,2 \cdot n}.$\shortv{\vspace{-1.5mm}}
\end{lemma}
% \shortv{
% \begin{proof}[Sketch]
% By induction on $k$, the number of reductions, exploiting Proposition \ref{p:cresce}.
% The base case holds trivially.
% For the inductive step 
% it is worth recalling that because of the limitations on the structure of the communicated objects their depth along reductions is \emph{always} bounded by $\depth{P}$. As a consequence, it is \emph{not} the case that the depth of the predecessor of $Q$ is $2^{k-1} \cdot n$.
% \qed
% \end{proof}
% }
\longv{
\begin{proof}
The proof proceeds by induction on $k$, the 
length of $\newarr^*$,
%number of reductions, 
exploiting Proposition \ref{p:cresce}.
The base case is when $k=1$, and it follows by Proposition \ref{p:cresce}.
For the inductive step we assume $k >1$, so we have that, for some $P'$,
%$P \arro{\alpha_1} \cdots \arro{\alpha_{k-1}} R \arro{\alpha_k} Q$.
$P \newarr^* P' \newarr Q$ where the sequence from $P$ to $P'$ has lenght $k-1$.
By induction hypothesis we know that $P' \in \mathcal{P}_{R,2 \cdot n}$. 
We then proceed by a case analysis on the rule used to infer $P' \newarr Q$.
As usual, we content ourselves with illustrating the case \textsc{Tau1}; the other ones are similar or simpler.
We then have that 
$P' = P_1 \parallel P_2$ 
with $P_1 \newarro{\Ho{a}{T}} S$ and $P_2 \newarro{a(x)} V$.
Hence $P_1 \equiv \outC{a}\langle T \rangle \parallel S$ and
$P_2 \equiv a(x).V$.
We then have that 
$P' \equiv \Ho{a}{T} \parallel S \parallel a(x).V$ and 
$Q \equiv V \sub T x \parallel S$.

%We then have that $P' \equiv x_1 \parallel \cdots \parallel x_k \parallel \Ho{a}{T} \parallel a(x).R' \parallel S$ 
%and that $Q \equiv x_1 \parallel \cdots \parallel x_k \parallel R'\sub T x  \parallel S$.

%Without loss of generality, we can assume 
%that $x$ is a leaf in the tree representation of process $R'$. Also, we can assume 
 % there is an input $b(y)$ at the top level of the process $T$, and that the bound variable $y$ is also a leaf in its tree representation. 
%The tree representation of $R$ is depicted in Figure \ref{f:red} (a). 

%It is worth recalling that by the syntax of \hof, all the free variables in (the tree representation of) $R'$ occur at the top level. Now consider the tree representation of $Q$, which is obtained by ``plugging in'' (the tree representation of) $T$ in the place of $x$ in $R'$. This is depicted in Figure \ref{f:red} (b): this might be helpful to understand that the largest distance between a variable and its binder is $n$, as formalized by Corollary \ref{c:bounddepth}. 
%Notice, for instance, that the distance between $y$ and its binder $b(y)$ in $T$ remains invariant after the reduction.
%We then conclude that because of the limitations on the structure of the communicated objects their depth along reductions is \emph{always} bounded by $\depth{P}$. Hence, $Q \in \mathcal{P}_{P,2 \cdot n}$, as wanted.

%  \begin{figure}[t]
%  \centering  
%  \subfigure[Tree representation of $R$]
%    {\includegraphics[width=5cm]{./img/figcinzia.pdf}}
%  \hspace{5mm}
%  \subfigure[Tree representation of $Q$]
%    {\includegraphics[width=5cm]{./img/figcinzia2.pdf}}
%  \caption{Tree representation of a reduction $R \newarr Q$, as in the proof of Lemma \ref{l:bound}.}\label{f:red}
%  \end{figure}

%The tree representation of process $R$ is depicted in Figure \ref{f:red} (a). There, $R''$ is used to represent a subprocess of $R'$. 
By Corollary \ref{c:bounddepth} 
the maximum distance between $x$ and its binder $a(x)$ is $\depth{P}$, which in turn is bounded by $n$ (Lemma \ref{l:depth}).  Moreover, the maximum depth of $T$ is bounded by $\maxDepCom{P}$; by Corollary \ref{c:bounddepth}, $\depth{P} \leq n$. 
%The tree representation of $Q$ is given in Figure \ref{f:red} (b).
Therefore, %We then conclude that because of the limitations on the structure of the communicated objects 
the overall depth of process $Q$ is $2 \cdot \depth{P}$. 
Hence, and by using Lemma \ref{l:depth}, $Q \in \mathcal{R}_{P,2 \cdot n}$, as wanted.
\qed
\end{proof}
}
\begin{corollary}\label{cor:deriv}
 Let $P \in \hof$. Then $\deriv{P} \subseteq \mathcal{P}_{P,2 \cdot \depth{P}}$.
\end{corollary}

\shortv{To prove that $\preceq$ is a wqo, we first show that it is a quasi order.}
\longv{We are now ready to prove that relation $\preceq$ is a wqo. We begin by showing that it is a quasi-order.}


\begin{proposition}
 The relation $\preceq$ is a quasi-order.%\vspace{-1.5mm}
\end{proposition}
% \shortv{
% \begin{proof}[Sketch]
% Follows from Definition \ref{def:nf} (normal form) and Lemma \ref{lem:nf}. \qed
% \end{proof}
% }
\longv{
\begin{proof}
We need to show that $\preceq$ is both reflexive and transitive. From Definition \ref{def:nf}, reflexivity is immediate. 

Transitivity implies proving that,  
given processes $P,Q$, and $R$ such that $P \preceq Q$ and $Q \preceq R$, $P \preceq R$ holds. 
We proceed by induction on $k = \depth{P}$. If $k = 0$ then we have that $P = x_1 \parallel \cdots \parallel x_k$.
Since $P \preceq Q$, we have that $Q = x_1 \parallel \cdots \parallel x_k \parallel S$. and that 
$R = x_1 \parallel \cdots \parallel x_k \parallel S'$, for some $S,S'$ such that $S \preceq S'$.
By Definition \ref{d:order}, the thesis follows. Now suppose $k > 0$. By Definition \ref{def:nf} and by hypothesis we have the following:
\begin{eqnarray*}
 P & = & \prod_{k=1}^{l} x_k \parallel \prod_{i=1}^{m} a_i(y_i) . P_i \parallel \prod_{j=1}^{n} \Ho{b_j}{P'_j} \\
Q & = & \prod_{k=1}^{l} x_k \parallel \prod_{i=1}^{m} a_i(y_i) . Q_i \parallel \prod_{j=1}^{n} \Ho{b_j}{Q'_j} \parallel S \\
R & = & \prod_{k=1}^{l} x_k \parallel \prod_{i=1}^{m} a_i(y_i) . R_i \parallel \prod_{j=1}^{n} \Ho{b_j}{R'_j} \parallel S \parallel T .
\end{eqnarray*}
with $P_i \preceq Q_i$,  $P'_j \preceq Q'_j$, $Q_i \preceq R_i$,  and $Q'_j \preceq R'_j$ ($i \in I, j \in J$).
Since $P_i$, $P'_j$, $Q_i$,  $Q'_j$, $R_i$,  and $R'_j$ have depth $k-1$, by inductive hypothesis
$P_i \preceq R_i$ and $P'_j \preceq R'_j$. By Definition \ref{d:order}, the thesis follows and we are done.
\qed
\end{proof}
}
We are now in place to state that $\preceq$ is a  wqo.

\begin{theorem}[Well-quasi-order]\label{th:wqo}
 Let $P \in \hof$ 
be a closed process
and $n \geq 0$. The relation $\preceq$ is a well-quasi-order over $\mathcal{P}_{P,n}$.%\vspace{-1.5mm}
\end{theorem}
\begin{proof}
The proof is by induction on $n$.

\longv{\begin{itemize}
 \item} \shortv{(--)} Let $n\!=\!0$. Then $\mathcal{P}_{P,0}$ contains processes containing only variables taken from  $\mathcal{A}(P)$. The equality on finite sets is
a well-quasi-ordering; by Lemma \ref{lem:Higman} (Higman's Lem\-ma) also $=_*$ is a well
quasi-ordering: it corresponds to the ordering $\preceq$
on processes containing only variables.

\longv{\item} \shortv{(--)} Let $n\!>\!0$. Take an infinite sequence of processes $s\! =\! P_1, P_2, \dots, P_l, \dots$ with $P_l \! \in \! \mathcal{P}_{P,n}$. We shall show that the thesis holds by means of successive filterings of the normal forms of the processes in $s$.
By Lemma \ref{lem:nf}  there exist $K_l,I_l$ and $J_l$ such that
%{\small 
$$P_l \equiv \prod_{k\in K_l} x_k \parallel \prod_{i\in I_l} a_i(y_i) . P^l_i \parallel \prod_{j\in J_l} \Ho{b_j}{P'^l_j}$$
%\vspace{-2mm}$$}
with $P^l_i$ and $P'^l_j \in \mathcal{P}_{P,n-1}$.  Hence each $P_l$ can be seen as composed of 3 finite sequences: (i) $ x_1 \dots x_k, \ $ (ii) $a_1(y_1).P^l_1 \dots a_i(y_i).P^l_i, \ $ and (iii)
$\Ho{b_1}{P'^l_1} \dots \Ho{b_j}{P'^l_j}$.
We note that the first sequence is composed of variables from the finite set $\mathcal{A}(P)$ whereas the other two sequences are composed by elements in $\mathcal{A}(P)$ and $\mathcal{P}_{P,n-1}$.
%
Since we have an infinite sequence of $\mathcal{A}(P)^*$, as $\mathcal{A}(P)$ is finite, by Proposition \ref{prop:eqwqo} and Lemma \ref{lem:Higman} we have that $=_*$ is a wqo over $\mathcal{A}(P)^*$.
%(the relation $=_*$ is defined according to Definition \ref{def:eqwqo} where we consider equality as the quasi-order on the starting set).
\longv{ 

}
By inductive hypothesis, we have that $\preceq$ is a wqo on $\mathcal{P}_{P,n-1}$, hence by Lemma \ref{lem:Higman} relation $\preceq_*$ is a wqo on $\mathcal{P}_{P,n-1}^*$.
We start filtering out $s$ by  making the finite sequences $x_1 \dots x_k$ increasing with respect to $=_*$; let us call this subsequence $t$. Then we filter out $t$,  by making the finite sequence $a_1(y_1).P^l_1 \dots a_i(y_i).P^l_i$ increasing with respect to both $=_*$  and  $\preceq_*$. This is done in two steps: first, by considering the relation
$=_*$ on the subject of the actions (recalling that $a_i, y_i \in \mathcal{A}(P)$), and second, 
by applying another filtering to the continuation  using the inductive hypothesis.  
%For the first step, i
It is worth remarking that in the first step we do not consider symbols
of the alphabet but pairs of symbols. Since the set
of pairs on a finite set is still finite, we know
by Higman's Lemma that $=_*$ is a wqo on the set of sequences of pairs $(a_i, y_i)$. 

For the sequence of outputs $\Ho{b_1}{P'^l_1} \dots \Ho{b_j}{P'^l_j}$ this is also done in two steps: the subject of the outputs are ordered with respect to $=_*$ and the objects of the output action are ordered with respect to $\preceq_*$ using the inductive hypothesis.

At the end of the process we obtain an infinite subsequence of $s$ that is ordered with respect to $\preceq$.
\longv{\end{itemize}}
\qed
\end{proof}
The last thing to show is that the well-quasi-ordering $\preceq$ is strongly compatible 
with respect to the 
%(finitely branching) 
LTS in Figure \ref{fig:newlts}.
%associated to \hof. 
We need some auxiliary results first.

\begin{lemma}\label{lem:paral}
 Let $P, P', Q$ and $Q'$ 
be  \hof processes in normal form such that $P \preceq P'$ and $Q \preceq Q'$.
Then it holds that $P \parallel Q \preceq P' \parallel Q'$.
\end{lemma}
\begin{proof}
 Immediate from the definitions of normal form and $\preceq$ (Definitions \ref{def:nf} and \ref{d:order}).
\qed
\end{proof}


\begin{lemma}\label{lem:subs}
 Let $P,P',Q$, and $Q'$ be  \hof processes in normal form such that $P \preceq P'$ and $Q \preceq Q'$. Then it holds that 
$P\sub{Q}{x} \preceq P'\sub{Q'}{x}$.
\end{lemma}
% \shortv{
% \begin{proof}\vspace{-1.5mm}
%  By induction on the structure of $P$.\qed
% \end{proof}
% }
\longv{
\begin{proof}
 By induction on the structure of $P$. 
\begin{enumerate}
 \item Cases $P = \nil$ and $P = y$, for some $y \neq x$: Immediate.
\item Case $P = x$. Then $P' = x \parallel N$, for some process $N$. We have that $P \sub Q x = Q$ and that $P' \sub {Q'} x = Q' \parallel N \sub {Q'} x$. Since $Q \preceq Q'$ the thesis follows.
\item Case $P = a(y).R$. Then $P' = a(y).R' \parallel N$, for some process $N$. 
Since by hypothesis $P \preceq P'$, then $R \preceq R'$. 
We then have that $P \sub Q x = a(y).R\sub Q x$ and that $P' \sub {Q'} x = a(y).R' \sub Q' x \parallel N \sub {Q'} x$.
By inductive hypothesis we obtain that $R \sub Q x \preceq R' \sub {Q'} x$, and the thesis follows.
\item Case $P = \Ho{a}{R}$: Similar to (3).
\item Case $P = R \parallel S$. Then $P' = R' \parallel S' \parallel N$, for some process $N$, with  $R \preceq R'$ and $S \preceq S'$.
We then have that $P \sub Q x = R \sub Q x \parallel S \sub Q x$ and $P' \sub {Q'} x = R' \sub {Q'} x \parallel S' \sub {Q'} x \parallel N \sub {Q'} x$. The thesis then follows by inductive hypothesis and Lemma \ref{lem:paral}.
\end{enumerate}
\qed
\end{proof}
}


\begin{theorem}[Strong Compatibility]\label{th:sc}
Let $P,Q,P' \in \hof$. If $P \preceq Q$ and $P \newarr P'$ then there exists $Q'$ such that $Q \newarr Q'$ and $P' \preceq Q'$. 
\end{theorem}
% \shortv{
% \begin{proof}\vspace{-1.5mm}
% By case analysis on the rule used to infer transition $\arro{\alpha}$, using Lemma \ref{lem:subs}.
% \qed 
% \end{proof}
% }
\longv{
\begin{proof}%\vspace{-1.5mm}
By case analysis on the rule used to infer reduction $P \newarr P'$. 
We content ourselves with illustrating the case 
derived from the use of rule
%\textsc{Inp} and 
\textsc{Tau1}; the other ones are similar or simpler.
%\begin{description}
% \item[Case \textsc{Inp}] Then $P = a(y).P_1$ and $Q = a(y).Q_1$, with $P_1 \preceq Q_1$. % and $N \preceq N'$. If $P \arro{a(y)} P' \equiv P_1$ then also $Q \arro{a(y)} Q' \equiv Q_1$. We then have that $P' \preceq Q'$, as desired.
%\item[Case \textsc{Tau1}]  
We then have that 
$P = P' \parallel P''$ %, $P' = P'_1 \parallel P'_2 \sub{R}{x}$, 
with $P' \newarro{\Ho{a}{P_1}} N$ and $P'' \newarro{a(y)} P_2$.
Hence, $P \equiv \Ho{a}{P_1} \parallel a(y).P_2 \parallel N$.
Since by hypothesis $P \preceq Q$, we obtain a similar structure for
$Q$. Indeed, 
$Q \equiv \Ho{a}{Q_1} \parallel a(y).Q_2 \parallel N'$ %, $P' = P'_1 \parallel P'_2 \sub{R}{x}$, 
with $P_1 \preceq Q_1$, $P_2 \preceq Q_2$, and $N \preceq N'$. 

Now, if $P \newarr P' \equiv P_2 \sub {P_1} y \parallel N$ then also 
$Q \newarr Q' \equiv Q_2 \sub {Q_1} y \parallel N'$.
By Lemma \ref{lem:subs} we have $P_2 \sub {P_1} y \preceq Q_2 \sub {Q_1} y$; using this and the hypothesis the thesis follows.
%\end{description}
\qed 
\end{proof}
}

\begin{theorem}\label{th:wsts}
 Let $P \in \hof$ be a closed process. 
The transition system $(\deriv{P}, \newarr, \preceq)$ is a finitely branching well-structured transition system with strong compatibility, decidable $\preceq$, and computable $Succ$.
\end{theorem}
\begin{proof}
 The transition system of \hof is finitely branching (Fact \ref{f:fb}). The fact that $\preceq$ is a well-quasi-order on $\deriv{P}$ follows from Corollary \ref{cor:deriv} and Theorem \ref{th:wqo}. Strong compatibility follows from Theorem \ref{th:sc}.
\qed \end{proof}


We can now state the main \longv{technical} result of the section. 
\shortv{It follows from Theorems \ref{th:Finkel} and \ref{th:wsts}.}

\begin{corollary}
Let $P \in \hof$ be a closed process. Then, termination of $P$ is decidable.
\end{corollary}
\longv{
\begin{proof}%\vspace{-1.5mm}
This follows from Theorem \ref{th:Finkel}, Theorem \ref{th:wsts}, and Corollary \ref{c:termination}.
\qed \end{proof}
}


